COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Collectors and Rules.
C00007 ENDMK
C⊗;
Collectors and Rules.

One of the more useful on-line facilities is the ability
to collect clauses together under names and refer to these 
collections in applying rules of inference or initiating  
subproofs.  
The addition of collectors and rules makes some of this online
ability available as a programmable artifact.
A collector is a pair consisting of a name and a pattern.  
Whenever clauses which match one of the collector patterns
are added to the prover's memory theses clauses are also added to
the symbol table entry for the collector's name.  Thus a collector
of UNIT,LENGTH=1 will automatically add to UNIT any unit clauses
which are generated(and retained).  Then if the user enters the editor
and types "DI UNITS;" he will see all the unit clauses.
Certainly we should allow the basic rules of inference to be applied
to the collectors, for this is a simple way to implement  many extra rules
of inference.
The rules which we currently allow must fit the following form:

	__________	__________
	|	 |	|	  |
	| C1(+)	 |	| C2(+)	  |
	|	 |	|	  |
	----------	-----------
		\	/
		  \   /
		________
		|	|
		|resolve|
		|	|
		---------	
		/  / \  \
	       C3 C4 C5...Cn

Ci's are collectors and the "+" is an optional suffix on C1 or C2.

The rule is applied in the following manner: Binary resolution is 
performed on the members of C1 and C2;  The current editing strategies
are applied and the resulting clauses,R, are added to the appropriate
collectors C3,...Cn. If the optional "+" is present the the set,R, is
also added to the appropriate Ci.

For example to express transitivity of a predicate,P, a rule of the 
following form will do:

C1: @P(x,y)∧P(y,z)⊃P(x,z); +
C2: UNITP
C3: UNITP

where: UNITP is the collector: LENGTH=1∧OCR[P]∧¬OCR[¬P]

Thus C1 begins with only the transitivity axiom; binary resoluton is
performed against C2,(unit clauses with predicate letter,P.)
The new clauses are added to C1 since + appears. Binary resolution is
performed again using C2 and the augmented set C1.  This time there will
be resolvents satisfying the pattern of UNITP. Any of these clauses
which satisfy the editing strategies are added to C2, and all of these edited
clauses are added to C1.  The cycle continues. If no more deductions can 
be made, the rule terminates.  

It is easy to give examples of rules of the above type which do not terminate.
Also the user frequently knows a bound to the useful applications of his rules.
For both of these reasons part of the definition of a rule is a bound on the
number of iterations to be performed.

Here are some more examples:

NAME		C1		C2		C3,...Cn

hyper		CLAUSES +	ALLPOS		ALLPOS
symm	    @P(x,y)⊃P(y,x);+	UNITP		UNITP
unitpf		CLAUSES +	UNIT		NIL
C-ded		CLAUSES +	C		CLAUSES